pre{-}init{-}p(${\it es}$; $i$; ${\it ds}$; ${\it init}$; $P$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$($\uparrow$($P$($\lambda$$x$.fpf{-}cap(${\it init}$;IdDeq;$x$;$\cdot$)))) $\Rightarrow$ ($\exists$$e$:es{-}E(${\it es}$). (es{-}loc(${\it es}$; $e$) = $i$ $\in$ Id))